\begin{tabbing}
$\forall$${\it the\_es}$:ES, ${\it e'}$:E, $l$:IdLnk, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$sends($l$;${\it e'}$)$\parallel$+1}}$.
\\[0ex]$\neg$snds($l$, before(${\it e'}$,$n$)) $=$ nil $\in$ (Msg on $l$) List
\\[0ex]$\Rightarrow$ (\=$\exists$$e$:E, $m$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$sends($l$;$e$)$\parallel$}}$.\+
\\[0ex]($e$ $<$loc ${\it e'}$) $\vee$ $e$ $=$ ${\it e'}$ \& $m$$<$$n$
\\[0ex]\& snds($l$, before(${\it e'}$,$n$)) $=$ (snds($l$, before($e$,$m$)) @ [sends($l$;$e$)[$m$]]) $\in$ (Msg on $l$) List
\\[0ex]\& (\=$\forall$${\it e''}$:E, $k$:$\mathbb{N}$.\+
\\[0ex]($e$ $<$loc ${\it e''}$) $\vee$ $e$ $=$ ${\it e''}$ \& $m$$<$$k$ \& (${\it e''}$ $<$loc ${\it e'}$) $\vee$ ${\it e''}$ $=$ ${\it e'}$ \& $k$$<$$n$
\\[0ex]$\Rightarrow$ $\parallel$sends($l$;${\it e''}$)$\parallel\leq$$k$))
\-\-
\end{tabbing}